Notes (Week 10 Wednesday)

(λx. f x) (λx. (λx. f x) x) y

(a) What are its free variables?

λx. is a binder of the name x, in the same way that ∀x. is

x ∧ ∀x. x ^free ^bound

(λx. f x) (λx. (λx. f x) x) y

y is free, and so is f

(b) What is its normal form?

(λx. t) s ↦β t[x:=s]

• remember that application is left-associative a b c (a b) c

(λx. f x) (λx. (λx. f x) x) y = ((λx. f x) (λx. (λx. f x) x)) y ↦β (f (λx. (λx. f x) x)) y ↦β (f (λx. f x)) y

A ⊕ B = (A ∧ B') ∨ (A' ∧ B)

(a)

A ⊕ A = (by definition) (A ∧ A') ∨ (A' ∧ A) = (complement) 0 ∨ (A' ∧ A) = (complement) 0 ∨ (A ∧ A') = (commutativity) 0 ∨ 0 = (identity) 0

(b) A ⊕ A' = (by definition) (A ∧ A'') ∨ (A' ∧ A') = (double complement) (A ∧ A) ∨ (A' ∧ A') = (idempotence) A ∨ A' = (complement) 1

(c) In the two-element boolean algebra we have:

(true ⊕ false)' = true' = false

(true' ⊕ false') = (false ⊕ true) = true

A real law:

A' ⊕ B' = A ⊕ B Another real law:

(A⊕B)' = A' ⊕ B

interleave(ab,cd) = acbd

interleave1(ab,cd) = a(interleave1(cd,b)) = ac(interleave1(b,d)) = acb(interleave1(d,λ)) = acbd(interleave1(λ,λ)) = acbdλ = acbd

(a) interleave(w,w') (i) |w|+|w'| (ii) |w| (iii) Let's define a WFO :)

(v',w') < (v,w) if:

v'

+

w'

<

v

+

w

or

v

+

w

=

v'

+

w'

and

v'

+2*

w'

<

v

+2*

w

^ what I defined here was the lexicographic combination of two wfo:s

If R ⊆ T × T and S ⊆ U × U are order relations, then their lexicographic combination:

R <lex S ⊆ (T × U) × (T × U)

((t,u),(t',u')) ∈ R <lex S if t R t' or t = t' and u R u'

The reason: If R and S are wfos, then R <lex S is also a wfo

interleave1(w,w') = interleave2(w,w')

• structural induction on w doesn't work :(

  IH interleave1(w,w') = interleave2(w,w')

  prove interleave1(aw,w') = a(interleave1(w',w)) = (stuck :( )) interleave2(aw,w')

Let's try: complete induction on |w|.

∀w'. interleave1(w,w') = interleave2(w,w')

I get an induction hypothesis:

IH: ∀w''. |w''| < |w| ⇒ ∀w'. interleave1(w'',w') = interleave2(w'',w')

Prove: interleave1(w,w') = interleave2(w,w') We need to do some case analysis on the structure of w,w'

Case 1: w = w' = λ

interleave1(λ,λ) = λ = interleave2(w,w')

Case 2: w = λ and w'=av

interleave1(λ,av) = av = interleave2(λ,av)

Case 3: w = av and w'=λ

interleave1(av,λ) = a(interleave1(λ,v)) = av

interleave2(av,λ) = av

Case 4: w = av and w'=bv'

interleave1(av,bv') = a(interleave1(bv',v)) = ab(interleave1(v,v')) = (IH) ab(interleave2(v,v')) = (def backwards) interleave2(av,bv')

Complete induction:

To prove ∀n. P(n) it suffices to prove ∀n. (∀m. m < n ⇒ P(m)) ⇒ P(n)

A ⊢ B __ (impI) ⊢ A → B

1 | A ↔ (B ∨ A)

2 | | B

-

3 | | B ∨ A ∨-I,2 4 | | A ↔-E 1,3 5 | B → A →-I 2-4

∃x. ∃y. (¬(x=y))

(a) is it satisfiable? Yes: any world with at least two domain elements satisfies this formula

(b) is it logically valid? "Logically valid" means "true in every model"

It is not logically valid because it is false in every model with exactly one domain element. (Philosophers and theologicans call this monism)

(c) - Natural deduction is sound and complete ND can prove exactly the logically valid statements.

• Therefore: no.

(a) liveness (b) reachability (c) safety

(d) A safety property states that some event never happens A liveness property states that some event will happen

(d') A safety property can be falsified by a finite prefix of a behaviour A liveness property: for any finite prefix, it can be extended into a behaviour that satisfies the liveness property (it's never too late to be live™)

r+ = rr*

(a) E(MRR*D)*Q (or if you prefer E(MR+D)*Q ) (b) - we cannot accept any word of length 1

• we can accept a word of length 2: EQ
• we can't accept any word of length 3: EMR …
• we can't accept any word of length 4: EMRD …
• we can accept a word of length 5: EMRDQ
• we can accept a word of length 5+n EMRR^nDQ

(c) ^ see above

{q==Q and r==R and s==S} # ← precondition {r==R and s==S and q==Q} t= q {r==R and s==S and t==Q} q= r {q==R and s==S and t==Q} r= s {q==R and r==S and t==Q} s= t {q==R and r==S and s==Q} # ← postcondition

(out of time)

[B] __ ∨-I A ∨ B A ↔ (A ∨ B) __ ↔-E A _ →I B → A

A ↔ (A ∨ B), B ⊢ B __ ∨-I A ∨ B A ↔ (A ∨ B) ⊢ A ↔ (A ∨ B) __ ↔-E A ↔ (A ∨ B), B ⊢ A _ →I A ↔ (A ∨ B) ⊢ B → A #+END_SRC